The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxTRS
↳3 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxWeightedTrs
↳7 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedTrs
↳9 CompletionProof (UPPER BOUND(ID), 0 ms)
↳10 CpxTypedWeightedCompleteTrs
↳11 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳12 CpxTypedWeightedCompleteTrs
↳13 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳14 CpxRNTS
↳15 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CpxRNTS
↳17 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳18 CpxRNTS
↳19 IntTrsBoundProof (UPPER BOUND(ID), 135 ms)
↳20 CpxRNTS
↳21 IntTrsBoundProof (UPPER BOUND(ID), 42 ms)
↳22 CpxRNTS
↳23 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳24 CpxRNTS
↳25 IntTrsBoundProof (UPPER BOUND(ID), 352 ms)
↳26 CpxRNTS
↳27 IntTrsBoundProof (UPPER BOUND(ID), 148 ms)
↳28 CpxRNTS
↳29 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳30 CpxRNTS
↳31 IntTrsBoundProof (UPPER BOUND(ID), 396 ms)
↳32 CpxRNTS
↳33 IntTrsBoundProof (UPPER BOUND(ID), 90 ms)
↳34 CpxRNTS
↳35 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳36 CpxRNTS
↳37 IntTrsBoundProof (UPPER BOUND(ID), 258 ms)
↳38 CpxRNTS
↳39 IntTrsBoundProof (UPPER BOUND(ID), 110 ms)
↳40 CpxRNTS
↳41 FinalProof (⇔, 0 ms)
↳42 BOUNDS(1, n^1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

double(0) → 0
double(s(x)) → s(s(double(x)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
if(0, y, z) → y
if(s(x), y, z) → z
half(double(x)) → x

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The TRS does not nest defined symbols.
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
half(double(x)) → x

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

double(0) → 0
double(s(x)) → s(s(double(x)))
half(s(0)) → 0
half(s(s(x))) → s(half(x))
if(s(x), y, z) → z
half(0) → 0
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
if(0, y, z) → y

Rewrite Strategy: INNERMOST

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

double(0) → 0 [1]
double(s(x)) → s(s(double(x))) [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
if(s(x), y, z) → z [1]
half(0) → 0 [1]
-(s(x), s(y)) → -(x, y) [1]
-(x, 0) → x [1]
if(0, y, z) → y [1]

Rewrite Strategy: INNERMOST

(5) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID) transformation)

Renamed defined symbols to avoid conflicts with arithmetic symbols:

- => minus

(6) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

double(0) → 0 [1]
double(s(x)) → s(s(double(x))) [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
if(s(x), y, z) → z [1]
half(0) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(x, 0) → x [1]
if(0, y, z) → y [1]

Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

double(0) → 0 [1]
double(s(x)) → s(s(double(x))) [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
if(s(x), y, z) → z [1]
half(0) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(x, 0) → x [1]
if(0, y, z) → y [1]

The TRS has the following type information:
double :: 0:s → 0:s
0 :: 0:s
s :: 0:s → 0:s
half :: 0:s → 0:s
if :: 0:s → if → if → if
minus :: 0:s → 0:s → 0:s

Rewrite Strategy: INNERMOST

(9) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:


double
half
if
minus

(c) The following functions are completely defined:
none

Due to the following rules being added:
none

And the following fresh constants:

const

(10) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

double(0) → 0 [1]
double(s(x)) → s(s(double(x))) [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
if(s(x), y, z) → z [1]
half(0) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(x, 0) → x [1]
if(0, y, z) → y [1]

The TRS has the following type information:
double :: 0:s → 0:s
0 :: 0:s
s :: 0:s → 0:s
half :: 0:s → 0:s
if :: 0:s → if → if → if
minus :: 0:s → 0:s → 0:s
const :: if

Rewrite Strategy: INNERMOST

(11) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(12) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

double(0) → 0 [1]
double(s(x)) → s(s(double(x))) [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
if(s(x), y, z) → z [1]
half(0) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(x, 0) → x [1]
if(0, y, z) → y [1]

The TRS has the following type information:
double :: 0:s → 0:s
0 :: 0:s
s :: 0:s → 0:s
half :: 0:s → 0:s
if :: 0:s → if → if → if
minus :: 0:s → 0:s → 0:s
const :: if

Rewrite Strategy: INNERMOST

(13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
const => 0

(14) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 }→ 1 + (1 + double(x)) :|: z' = 1 + x, x >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(x) :|: x >= 0, z' = 1 + (1 + x)
if(z', z'', z1) -{ 1 }→ y :|: z1 = z, z >= 0, z'' = y, y >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z :|: z' = 1 + x, z1 = z, z >= 0, z'' = y, x >= 0, y >= 0
minus(z', z'') -{ 1 }→ x :|: z'' = 0, z' = x, x >= 0
minus(z', z'') -{ 1 }→ minus(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y

(15) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(16) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 }→ 1 + (1 + double(z' - 1)) :|: z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
minus(z', z'') -{ 1 }→ minus(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0

(17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ double }
{ minus }
{ if }
{ half }

(18) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 }→ 1 + (1 + double(z' - 1)) :|: z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
minus(z', z'') -{ 1 }→ minus(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0

Function symbols to be analyzed: {double}, {minus}, {if}, {half}

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)


Computed SIZE bound using CoFloCo for: double
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: 2·z'

(20) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 }→ 1 + (1 + double(z' - 1)) :|: z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
minus(z', z'') -{ 1 }→ minus(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0

Function symbols to be analyzed: {double}, {minus}, {if}, {half}
Previous analysis results are:
double: runtime: ?, size: O(n1) [2·z']

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)


Computed RUNTIME bound using CoFloCo for: double
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: 1 + z'

(22) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 }→ 1 + (1 + double(z' - 1)) :|: z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
minus(z', z'') -{ 1 }→ minus(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0

Function symbols to be analyzed: {minus}, {if}, {half}
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']

(23) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(24) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 + z' }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z' - 1), z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
minus(z', z'') -{ 1 }→ minus(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0

Function symbols to be analyzed: {minus}, {if}, {half}
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)


Computed SIZE bound using KoAT for: minus
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: z'

(26) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 + z' }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z' - 1), z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
minus(z', z'') -{ 1 }→ minus(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0

Function symbols to be analyzed: {minus}, {if}, {half}
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']
minus: runtime: ?, size: O(n1) [z']

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)


Computed RUNTIME bound using CoFloCo for: minus
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: 1 + z''

(28) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 + z' }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z' - 1), z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
minus(z', z'') -{ 1 }→ minus(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0

Function symbols to be analyzed: {if}, {half}
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']
minus: runtime: O(n1) [1 + z''], size: O(n1) [z']

(29) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(30) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 + z' }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z' - 1), z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 + z'' }→ s' :|: s' >= 0, s' <= 1 * (z' - 1), z' - 1 >= 0, z'' - 1 >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0

Function symbols to be analyzed: {if}, {half}
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']
minus: runtime: O(n1) [1 + z''], size: O(n1) [z']

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)


Computed SIZE bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: z'' + z1

(32) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 + z' }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z' - 1), z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 + z'' }→ s' :|: s' >= 0, s' <= 1 * (z' - 1), z' - 1 >= 0, z'' - 1 >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0

Function symbols to be analyzed: {if}, {half}
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']
minus: runtime: O(n1) [1 + z''], size: O(n1) [z']
if: runtime: ?, size: O(n1) [z'' + z1]

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)


Computed RUNTIME bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(34) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 + z' }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z' - 1), z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 + z'' }→ s' :|: s' >= 0, s' <= 1 * (z' - 1), z' - 1 >= 0, z'' - 1 >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0

Function symbols to be analyzed: {half}
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']
minus: runtime: O(n1) [1 + z''], size: O(n1) [z']
if: runtime: O(1) [1], size: O(n1) [z'' + z1]

(35) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(36) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 + z' }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z' - 1), z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 + z'' }→ s' :|: s' >= 0, s' <= 1 * (z' - 1), z' - 1 >= 0, z'' - 1 >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0

Function symbols to be analyzed: {half}
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']
minus: runtime: O(n1) [1 + z''], size: O(n1) [z']
if: runtime: O(1) [1], size: O(n1) [z'' + z1]

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)


Computed SIZE bound using KoAT for: half
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: z'

(38) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 + z' }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z' - 1), z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 + z'' }→ s' :|: s' >= 0, s' <= 1 * (z' - 1), z' - 1 >= 0, z'' - 1 >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0

Function symbols to be analyzed: {half}
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']
minus: runtime: O(n1) [1 + z''], size: O(n1) [z']
if: runtime: O(1) [1], size: O(n1) [z'' + z1]
half: runtime: ?, size: O(n1) [z']

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)


Computed RUNTIME bound using PUBS for: half
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: 1 + z'

(40) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 + z' }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z' - 1), z' - 1 >= 0
half(z') -{ 1 }→ 0 :|: z' = 1 + 0
half(z') -{ 1 }→ 0 :|: z' = 0
half(z') -{ 1 }→ 1 + half(z' - 2) :|: z' - 2 >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z1 >= 0, z'' >= 0, z' = 0
if(z', z'', z1) -{ 1 }→ z1 :|: z1 >= 0, z' - 1 >= 0, z'' >= 0
minus(z', z'') -{ 1 + z'' }→ s' :|: s' >= 0, s' <= 1 * (z' - 1), z' - 1 >= 0, z'' - 1 >= 0
minus(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0

Function symbols to be analyzed:
Previous analysis results are:
double: runtime: O(n1) [1 + z'], size: O(n1) [2·z']
minus: runtime: O(n1) [1 + z''], size: O(n1) [z']
if: runtime: O(1) [1], size: O(n1) [z'' + z1]
half: runtime: O(n1) [1 + z'], size: O(n1) [z']

(41) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(42) BOUNDS(1, n^1)